2023
Contribution to book
Open Access
A case study in formal analysis of system requirements
Belli D., Mazzanti F.
One of the goals of the 4SECURail project has been to demonstrate the benefits, limits, and costs of introducing formal meth- ods in the system requirements definition process. This has been done, on an experimental basis, by applying a specific set of tools and method- ologies to a case study from the railway sector. The paper describes the approach adopted in the project and some considerations resulting from the experience.Source: Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, edited by Masci P., Bernardeschi C., Graziani P., Koddenbrock M., Palmieri M., pp. 164–173, 2023
DOI: 10.1007/978-3-031-26236-4_14
Project(s): 4SECURAIL
Metrics:
Belli D., Mazzanti F.
One of the goals of the 4SECURail project has been to demonstrate the benefits, limits, and costs of introducing formal meth- ods in the system requirements definition process. This has been done, on an experimental basis, by applying a specific set of tools and method- ologies to a case study from the railway sector. The paper describes the approach adopted in the project and some considerations resulting from the experience.Source: Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, edited by Masci P., Bernardeschi C., Graziani P., Koddenbrock M., Palmieri M., pp. 164–173, 2023
DOI: 10.1007/978-3-031-26236-4_14
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository 
| doi.org 
| link.springer.com | CNR ExploRA
2023
Conference article
Open Access
Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect
Basile D., Mazzanti F., Ferrari A.
The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into industrial model-based development tools has been the subject of recent research, indicating the potential transfer of academic techniques to enhance industrial tools. This paper explores the integration of an academic formal verification tool, UML Model Checker (UMC), with an industrial model-based development tool, Sparx Enterprise Architect (Sparx EA). The case study being analyzed is a railway standard interface. The paper demonstrates how formal verification techniques from academic tools can be integrated into industrial development practices using industrial tools, and how simulation in Sparx EA can be derived from traces generated by the UMC formal verification activity. From this experience, we derive a set of lessons learned and research challenges.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 1–21, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_1
Project(s): 4SECURAIL
Metrics:
Basile D., Mazzanti F., Ferrari A.
The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into industrial model-based development tools has been the subject of recent research, indicating the potential transfer of academic techniques to enhance industrial tools. This paper explores the integration of an academic formal verification tool, UML Model Checker (UMC), with an industrial model-based development tool, Sparx Enterprise Architect (Sparx EA). The case study being analyzed is a railway standard interface. The paper demonstrates how formal verification techniques from academic tools can be integrated into industrial development practices using industrial tools, and how simulation in Sparx EA can be derived from traces generated by the UMC formal verification activity. From this experience, we derive a set of lessons learned and research challenges.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 1–21, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_1
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Software
Unknown
Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect - Complementary data
Basile D., Mazzanti F., Ferrari A.
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
Basile D., Mazzanti F., Ferrari A.
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
See at: CNR ExploRA
2023
Conference article
Open Access
The 4SECURail case study on rigorous standard interface specifications
Belli D., Fantechi A., Gnesi S., Masullo L., Mazzanti F., Quadrini L., Trentini D., Vaghi C.
In the context of the Shift2Rail open call S2R-OC-IP2-01- 2019, one of the two work streams of the 4SECURail project has pursued the objective to corroborate how a clear, rigorous standard interface specification between signaling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at illustrating some usable state-of-the-art techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 22–39, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_2
Project(s): 4SECURAIL
Metrics:
Belli D., Fantechi A., Gnesi S., Masullo L., Mazzanti F., Quadrini L., Trentini D., Vaghi C.
In the context of the Shift2Rail open call S2R-OC-IP2-01- 2019, one of the two work streams of the 4SECURail project has pursued the objective to corroborate how a clear, rigorous standard interface specification between signaling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at illustrating some usable state-of-the-art techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 22–39, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_2
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2022
Journal article
Open Access
Efficient static analysis and verification of featured transition systems
Ter Beek M. H., Damiani F., Lienhardt M., Mazzanti F., Paolini L.
A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification - if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.Source: Empirical software engineering (Online) 27 (2022). doi:10.1007/s10664-020-09930-8
DOI: 10.1007/s10664-020-09930-8
Metrics:
Ter Beek M. H., Damiani F., Lienhardt M., Mazzanti F., Paolini L.
A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification - if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.Source: Empirical software engineering (Online) 27 (2022). doi:10.1007/s10664-020-09930-8
DOI: 10.1007/s10664-020-09930-8
Metrics:
See at:
link.springer.com | ISTI Repository | ISTI Repository | CNR ExploRA
2022
Conference article
Open Access
Formal modeling and initial analysis of the 4SECURail case study
Mazzanti F., Belli D.
We present the case study developed in the context of the 4SECURail project and the approach used for its formal modeling and analysis. Starting from a simple SysML/UML behavioral model of the system requirements, three formal models have been developed using three different frameworks, namely UMC, ProB, and CADP/LNT. The paper shows how the different ways to represent and analyze the system from the three different points of view allow us to take advantage of the resulting diversity.Source: MARS 2022 - Fifth Workshop on Models for Formal Analysis of Real Systems, pp. 118–144, Munich, DE, 01/04/2022
DOI: 10.4204/eptcs.355.6
Project(s): 4SECURAIL
Metrics:
Mazzanti F., Belli D.
We present the case study developed in the context of the 4SECURail project and the approach used for its formal modeling and analysis. Starting from a simple SysML/UML behavioral model of the system requirements, three formal models have been developed using three different frameworks, namely UMC, ProB, and CADP/LNT. The paper shows how the different ways to represent and analyze the system from the three different points of view allow us to take advantage of the resulting diversity.Source: MARS 2022 - Fifth Workshop on Models for Formal Analysis of Real Systems, pp. 118–144, Munich, DE, 01/04/2022
DOI: 10.4204/eptcs.355.6
Project(s): 4SECURAIL
Metrics:
See at:
eptcs.web.cse.unsw.edu.au | ISTI Repository | CNR ExploRA
2022
Journal article
Open Access
FTS4VMC: a front-end tool for static analysis and family-based model checking of FTSs with VMC
Ter Beek M. H., Damiani F., Lienhardt M., Mazzanti F., Paolini L., Scarso G.
FTS4VMC is a publicly available front-end tool for the static analysis and family-based model checking of a Featured Transition System (FTS). It can detect ambiguities in an FTS, disambiguate an ambiguous FTS, transform an FTS into a Modal Transition System (MTS), and interact with the VMC model checker for family-based verification.Source: Science of computer programming (Print) 224 (2022). doi:10.1016/j.scico.2022.102879
DOI: 10.1016/j.scico.2022.102879
Metrics:
Ter Beek M. H., Damiani F., Lienhardt M., Mazzanti F., Paolini L., Scarso G.
FTS4VMC is a publicly available front-end tool for the static analysis and family-based model checking of a Featured Transition System (FTS). It can detect ambiguities in an FTS, disambiguate an ambiguous FTS, transform an FTS into a Modal Transition System (MTS), and interact with the VMC model checker for family-based verification.Source: Science of computer programming (Print) 224 (2022). doi:10.1016/j.scico.2022.102879
DOI: 10.1016/j.scico.2022.102879
Metrics:
See at:
ISTI Repository | www.sciencedirect.com | CNR ExploRA
2022
Conference article
Open Access
The 4SECURail formal methods demonstrator
Mazzanti F., Belli D.
The need for high-quality standard interfaces is widely recognized as a mandatory step to reduce procurement costs and create safely operating complex railway infrastructures. That is why European initiatives like EULYNX have been set up precisely with the purpose of supporting standard interfaces development. The exploitation of formal methods during the phase of standardization plays an essential role in raising the quality of the generated specifications. 4SECURail is a recent project that aims to precisely show, with a structured evaluation (known as the formal methods demonstrator), how formal methods might help to improve the quality of a specific signalling interface selected as case study. This paper describes the experience gained with the experiment.Source: RSSRail 2022 - 4th International Conference on Reliability, Safety, and Security of Railway Systems, pp. 149–165, Paris, France, 1-2/06/2022
DOI: 10.1007/978-3-031-05814-1_11
DOI: 10.5281/zenodo.6245955
DOI: 10.5281/zenodo.6245956
Project(s): 4SECURAIL
Metrics:
Mazzanti F., Belli D.
The need for high-quality standard interfaces is widely recognized as a mandatory step to reduce procurement costs and create safely operating complex railway infrastructures. That is why European initiatives like EULYNX have been set up precisely with the purpose of supporting standard interfaces development. The exploitation of formal methods during the phase of standardization plays an essential role in raising the quality of the generated specifications. 4SECURail is a recent project that aims to precisely show, with a structured evaluation (known as the formal methods demonstrator), how formal methods might help to improve the quality of a specific signalling interface selected as case study. This paper describes the experience gained with the experiment.Source: RSSRail 2022 - 4th International Conference on Reliability, Safety, and Security of Railway Systems, pp. 149–165, Paris, France, 1-2/06/2022
DOI: 10.1007/978-3-031-05814-1_11
DOI: 10.5281/zenodo.6245955
DOI: 10.5281/zenodo.6245956
Project(s): 4SECURAIL
Metrics:
See at:
ZENODO | ZENODO | ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2022
Conference article
Open Access
The 4SECURail approach to formalizing standard interfaces between signalling systems components
Belli D., Fantechi A., Gnesi S., Masullo L., Mazzanti F., Pistilli G., Quadrini L., Trentini D., Vaghi C.
In the context of the Shift2Rail open call S2R-OC-IP2-01-2019, one of the two work streams of the 4SECURail project (GA 881775) pursues the objective to corroborate how a clear, rigorous standard interface specification between signalling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at consolidating the most suitable techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments. This paper discusses the main results of the project.Source: Transport Research Arena (TRA) Conference, Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL
Belli D., Fantechi A., Gnesi S., Masullo L., Mazzanti F., Pistilli G., Quadrini L., Trentini D., Vaghi C.
In the context of the Shift2Rail open call S2R-OC-IP2-01-2019, one of the two work streams of the 4SECURail project (GA 881775) pursues the objective to corroborate how a clear, rigorous standard interface specification between signalling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at consolidating the most suitable techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments. This paper discusses the main results of the project.Source: Transport Research Arena (TRA) Conference, Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL
See at:
ISTI Repository | CNR ExploRA
2021
Journal article
Open Access
Compositional verification of concurrent systems by combining bisimulations
Frédéric Lang F., Mateescu R., Mazzanti F.
One approach to verify a property expressed as a modal ?-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes in a hierarchical way, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Ldbr fragment? of the ?-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching for short) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or div-branching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend Ldbr with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems. In particular, we applied our approach to the verification problems of the RERS 2019 challenge and observed drastic reductions of the state space compared to the approach in which only strong bisimulation minimization is used, on formulas not preserved by divbranching bisimulation.Source: Formal methods in system design (Dordr., Online) (2021). doi:10.1007/s10703-021-00360-w
DOI: 10.1007/s10703-021-00360-w
DOI: 10.1007/978-3-030-30942-8_13
Project(s): 4SECURAIL
Metrics:
Frédéric Lang F., Mateescu R., Mazzanti F.
One approach to verify a property expressed as a modal ?-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes in a hierarchical way, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Ldbr fragment? of the ?-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching for short) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or div-branching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend Ldbr with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems. In particular, we applied our approach to the verification problems of the RERS 2019 challenge and observed drastic reductions of the state space compared to the approach in which only strong bisimulation minimization is used, on formulas not preserved by divbranching bisimulation.Source: Formal methods in system design (Dordr., Online) (2021). doi:10.1007/s10703-021-00360-w
DOI: 10.1007/s10703-021-00360-w
DOI: 10.1007/978-3-030-30942-8_13
Project(s): 4SECURAIL
Metrics:
See at:
hal.inria.fr | Formal Methods in System Design | ISTI Repository | doi.org | Formal Methods in System Design | INRIA a CCSD electronic archive server | HAL Descartes | link.springer.com | CNR ExploRA
2021
Report
Open Access
4SECURail - Technical Informative Note 15 - Progress Report: Formal development Demonstrator Prototype
Mazzanti F., Belli D.
This Technical Informative Note describes the progress of the activity of Work Package 2 / Task 2.3 in the months 12-17 of the project 4SECURail. The final results of Task 2.3 will be described in Deliverable 2.5, due at month 20 (end of July 2021). This Technical Informative Note is likely to already contain most of the interesting results that will appear in the final deliverable, together with other less important internal progress details that for readability issues will not appear in the final version. The overall final purpose of the whole experimentation is the observation of the impact, in our specific case, i.e. applying our specific tools and methodologies1 to our specific case study2, of the adoption of formal methods towards the improvement of the quality of the system specifications under construction.Source: Project report, 4SECURail, TIN-FM-15, pp.1–53, 2021
Project(s): 4SECURAIL
Mazzanti F., Belli D.
This Technical Informative Note describes the progress of the activity of Work Package 2 / Task 2.3 in the months 12-17 of the project 4SECURail. The final results of Task 2.3 will be described in Deliverable 2.5, due at month 20 (end of July 2021). This Technical Informative Note is likely to already contain most of the interesting results that will appear in the final deliverable, together with other less important internal progress details that for readability issues will not appear in the final version. The overall final purpose of the whole experimentation is the observation of the impact, in our specific case, i.e. applying our specific tools and methodologies1 to our specific case study2, of the adoption of formal methods towards the improvement of the quality of the system specifications under construction.Source: Project report, 4SECURail, TIN-FM-15, pp.1–53, 2021
Project(s): 4SECURAIL
See at:
ISTI Repository | CNR ExploRA
2021
Report
Open Access
Systematic evaluation and usability analysis of formal tools for railway system design
Ferrari A., Mazzanti F., Basile D., Ter Beek M. H.
Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal tools to adopt in their contexts, a clear assessment of the features of the currently available tools is required. To address this goal, this paper considers a set of 13 formal tools that have been used for railway system design, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools.Source: ISTI-2021-TR/007, 2021
DOI: 10.32079/isti-tr-2021/007
Project(s): 4SECURAIL, ASTRail
Metrics:
Ferrari A., Mazzanti F., Basile D., Ter Beek M. H.
Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal tools to adopt in their contexts, a clear assessment of the features of the currently available tools is required. To address this goal, this paper considers a set of 13 formal tools that have been used for railway system design, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools.Source: ISTI-2021-TR/007, 2021
DOI: 10.32079/isti-tr-2021/007
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
ISTI Repository | CNR ExploRA
2021
Conference article
Open Access
Static analysis and family-based model checking of featured transition systems with VMC
Ter Beek M. H., Mazzanti F., Damiani F., Paolini L., Scarso G., Valfrè M., Lienhardt M.
A Featured Transition System (FTS) is a formalism for modeling variability in configurable system behavior. The behavior of all variants (products) is modeled in a single compact FTS by associating the possibility to perform an action and transition from one state to another with feature expressions that condition the execution of an action in specific variants. We present a front-end for the research tool VMC. The resulting toolchain allows a modeler to analyze an FTS for ambiguities (dead or false optional transitions and hidden deadlock states), transform an ambiguous FTS into an unambiguous one, and perform an efficient kind of family-based verification of an FTS without hidden deadlock states. We use benchmarks from the literature to demonstrate the novelties offered by the toolchain.Source: SPLC'21 - 25th ACM International Systems and Software Product Line Conference, pp. 24–27, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461002.3473071
Metrics:
Ter Beek M. H., Mazzanti F., Damiani F., Paolini L., Scarso G., Valfrè M., Lienhardt M.
A Featured Transition System (FTS) is a formalism for modeling variability in configurable system behavior. The behavior of all variants (products) is modeled in a single compact FTS by associating the possibility to perform an action and transition from one state to another with feature expressions that condition the execution of an action in specific variants. We present a front-end for the research tool VMC. The resulting toolchain allows a modeler to analyze an FTS for ambiguities (dead or false optional transitions and hidden deadlock states), transform an ambiguous FTS into an unambiguous one, and perform an efficient kind of family-based verification of an FTS without hidden deadlock states. We use benchmarks from the literature to demonstrate the novelties offered by the toolchain.Source: SPLC'21 - 25th ACM International Systems and Software Product Line Conference, pp. 24–27, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461002.3473071
Metrics:
See at:
ISTI Repository | dl.acm.org | CNR ExploRA
2021
Conference article
Open Access
Static analysis and family-based model checking with VMC
Ter Beek M. H., Mazzanti F., Damiani F., Paolini L., Scarso G., Lienhardt M.
VMC is a research tool for model checking variability-rich behavioural models specified as a modal transition system (MTS) with variability constraints (MTSv). In this tutorial, we introduce a tool chain built on VMC that allows to perform an efficient kind of family-based model checking in absence of deadlocks. It accepts as input either an MTSv or a featured transition system (FTS).Source: SPLC'21 - 25th International Systems and Software Product Line Conference, pp. 214–214, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461001.3472732
Metrics:
Ter Beek M. H., Mazzanti F., Damiani F., Paolini L., Scarso G., Lienhardt M.
VMC is a research tool for model checking variability-rich behavioural models specified as a modal transition system (MTS) with variability constraints (MTSv). In this tutorial, we introduce a tool chain built on VMC that allows to perform an efficient kind of family-based model checking in absence of deadlocks. It accepts as input either an MTSv or a featured transition system (FTS).Source: SPLC'21 - 25th International Systems and Software Product Line Conference, pp. 214–214, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461001.3472732
Metrics:
See at:
ISTI Repository | ISTI Repository | dl.acm.org | CNR ExploRA
2021
Report
Open Access
4SECURail - Revised requirements of the 4SECURail case study
Mazzanti F., Belli D.
The final version of the system requirements of the case study used in the 4SECURail demonstratorSource: ISTI Project report, 4SECURail, 2021
DOI: 10.5281/zenodo.5541217
Project(s): 4SECURAIL
Metrics:
Mazzanti F., Belli D.
The final version of the system requirements of the case study used in the 4SECURail demonstratorSource: ISTI Project report, 4SECURail, 2021
DOI: 10.5281/zenodo.5541217
Project(s): 4SECURAIL
Metrics:
See at:
ISTI Repository | CNR ExploRA
2021
Software
Unknown
Formal models of the SAI/CSL system of the 4SECURail case study
Mazzanti F., Belli D.
Formal models of 4SECURAIL case study in the notation accepted by UMC, ProB, CADP/LNTDOI: 10.5281/zenodo.5541307
Project(s): 4SECURAIL
Metrics:
Mazzanti F., Belli D.
Formal models of 4SECURAIL case study in the notation accepted by UMC, ProB, CADP/LNTDOI: 10.5281/zenodo.5541307
Project(s): 4SECURAIL
Metrics:
See at: CNR ExploRA
2021
Software
Unknown
The UMC2LNT and UMC2PROB model transformation tools
Mazzanti F., Belli D.
This documents contains the source code of two trasformation tools used in the 4SECURail project. The tools umc2lnt takes as argument the name of a file contining an UMC model and generates the corresponding CADP/LNT model.DOI: 10.5281/zenodo.5541350
Project(s): 4SECURAIL
Metrics:
Mazzanti F., Belli D.
This documents contains the source code of two trasformation tools used in the 4SECURail project. The tools umc2lnt takes as argument the name of a file contining an UMC model and generates the corresponding CADP/LNT model.DOI: 10.5281/zenodo.5541350
Project(s): 4SECURAIL
Metrics:
See at: CNR ExploRA
2021
Report
Open Access
4SECURail - Formal development demonstrator prototype, final release
Mazzanti F., Belli D.
This Deliverable describes the final results of Task 2.3 of 4SECURail project. The goal of Task 2.3 is to apply the formal development demonstrator process defined in Task 2.1 to the signalling case study defined in Task 2.2 and to describe the observed impact of the selected tools and methodologies for improving the quality of the system specifications under analysis.Source: ISTI Project report, 4SECURail, 2021
Project(s): 4SECURAIL
Mazzanti F., Belli D.
This Deliverable describes the final results of Task 2.3 of 4SECURail project. The goal of Task 2.3 is to apply the formal development demonstrator process defined in Task 2.1 to the signalling case study defined in Task 2.2 and to describe the observed impact of the selected tools and methodologies for improving the quality of the system specifications under analysis.Source: ISTI Project report, 4SECURail, 2021
Project(s): 4SECURAIL
See at:
ISTI Repository | CNR ExploRA
2021
Journal article
Open Access
Systematic evaluation and usability analysis of formal methods tools for railway signaling system design
Ferrari A., Mazzanti F., Basile D., Ter Beek M. H.
Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal methods tools to adopt in their contexts, a clear assessment of the features of the currently available tools is required. To address this goal, this paper considers a set of 13 formal methods tools that have been used for the early design of railway systems, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway signaling domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal methods tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools. Our contribution can be useful to R&D engineers from railway signaling companies and infrastructure managers, but also to tool developers and academic researchers alike.Source: IEEE transactions on software engineering 48 (2021): 4675–4691. doi:10.1109/TSE.2021.3124677
DOI: 10.1109/tse.2021.3124677
Project(s): 4SECURAIL, ASTRail
Metrics:
Ferrari A., Mazzanti F., Basile D., Ter Beek M. H.
Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal methods tools to adopt in their contexts, a clear assessment of the features of the currently available tools is required. To address this goal, this paper considers a set of 13 formal methods tools that have been used for the early design of railway systems, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway signaling domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal methods tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools. Our contribution can be useful to R&D engineers from railway signaling companies and infrastructure managers, but also to tool developers and academic researchers alike.Source: IEEE transactions on software engineering 48 (2021): 4675–4691. doi:10.1109/TSE.2021.3124677
DOI: 10.1109/tse.2021.3124677
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
ISTI Repository | ieeexplore.ieee.org | CNR ExploRA
2020
Conference article
Open Access
Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
Lang F., Mateescu R., Mazzanti F.
We showed in a recent paper that, when verifying a modal?-calculus formula, the actions of the system under verification can bepartitioned into sets of so-called weak and strong actions, depending onthe combination of weak and strong modalities occurring in the formula.In a compositional verification setting, where the system consists of pro-cesses executing in parallel, this partition allows us to decide whethereach individual process can be minimized for either divergence-preservingbranching (if the process contains only weak actions) or strong (other-wise) bisimilarity, while preserving the truth value of the formula. In thispaper, we refine this idea by devising a family of bisimilarity relations,named sharp bisimilarities, parameterized by the set of strong actions.We show that these relations have all the nice properties necessary tobe used for compositional verification, in particular congruence and ad-equacy with the logic. We also illustrate their practical utility on severalexamples and case-studies, and report about our success in the RERS2019 model checking challenge.Source: 26th International Conference, TACAS 2020, pp. 57–73, Dublin, Ireland, April 25-30, 2020
DOI: 10.1007/978-3-030-45237-7_4
Metrics:
Lang F., Mateescu R., Mazzanti F.
We showed in a recent paper that, when verifying a modal?-calculus formula, the actions of the system under verification can bepartitioned into sets of so-called weak and strong actions, depending onthe combination of weak and strong modalities occurring in the formula.In a compositional verification setting, where the system consists of pro-cesses executing in parallel, this partition allows us to decide whethereach individual process can be minimized for either divergence-preservingbranching (if the process contains only weak actions) or strong (other-wise) bisimilarity, while preserving the truth value of the formula. In thispaper, we refine this idea by devising a family of bisimilarity relations,named sharp bisimilarities, parameterized by the set of strong actions.We show that these relations have all the nice properties necessary tobe used for compositional verification, in particular congruence and ad-equacy with the logic. We also illustrate their practical utility on severalexamples and case-studies, and report about our success in the RERS2019 model checking challenge.Source: 26th International Conference, TACAS 2020, pp. 57–73, Dublin, Ireland, April 25-30, 2020
DOI: 10.1007/978-3-030-45237-7_4
Metrics:
See at:
doi.org | Europe PubMed Central | link.springer.com | link.springer.com | ISTI Repository | INRIA a CCSD electronic archive server | CNR ExploRA